﻿<?xml version="1.0" encoding="utf-8"?><!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"><html>
<!-- saved from url=(0033)http://research.microsoft.com/pex -->
<head><link rel="StyleSheet" href="er.common.css" type="text/css" /><script src="er.common.js" type="text/javascript"> </script><link rel="SHORTCUT ICON" href="favicon.ico" /><link rel="icon" href="favicon.ico" type="image/x-icon" /><title>C:\Users\AO\Documents\Visual Studio 2010\AutomaTones3\automatones\AutomaTones\AutomaTones\Model\Automaton Model\State.cs</title></head><body><div class="banner"></div><h2 id="top">C:\Users\AO\Documents\Visual Studio 2010\AutomaTones3\automatones\AutomaTones\AutomaTones\Model\Automaton Model\State.cs</h2><div class="toggle"><p class="copyright"><a class="usercodeundertestcovered">user code under test</a>, 
  <span class="usercodeundertestnotcovered">user code under test (not covered)</span>, 
  <a class="userortestcodecovered">user code or test</a>, 
  <span class="userortestcodenotcovered">user code or test (not covered)</span>,
  <span class="tagged">tagged</span></p><table><tr><th>Methods</th></tr><tr><th /></tr></table><div class="toggle"><a class="button" href="#ID0EL">first</a><pre class="coverage">using System;
using System.Diagnostics.Contracts;

namespace AutomaTones.Model.Automaton_Model {
    /// &lt;author&gt;Anders Øland / anoe@itu.dk&lt;/author&gt;
    /// &lt;summary&gt;
    /// The state of a cell represented by a discrete value within a given state space.. 
    /// NOTE: Ideally this would be implemented using generics so states could also be decimals.
    /// NOTE: But due to C#'s lack of type constraint options on value types - this was omitted.
    /// &lt;/summary&gt;
    [Serializable]
    public class State {
        /// &lt;summary&gt;
        /// The lower boundary of the state space.
        /// &lt;/summary&gt;
        public int SpaceMin { get; protected set; }

        /// &lt;summary&gt;
        /// The upper boundary of the state space.
        /// &lt;/summary&gt;
        public int SpaceMax { get; protected set; }

        private int _currentState;

        /// &lt;summary&gt;
        /// Current state.
        /// &lt;/summary&gt;
        public int CurrentState {
            get <span id="ID0EL"><a class="button" href="#top">top</a>|<a class="button" href="#ID0ELC">next</a></span><a class="userortestcodecovered">{</a> <a class="userortestcodecovered">return _currentState;</a> <a class="userortestcodecovered">}</a>
            protected internal set <a class="button" href="#ID0EL">prev</a>|<span id="ID0ELC"><a class="button" href="#top">top</a>|<a class="button" href="#ID0EPE">next</a></span><a class="userortestcodecovered">{</a>
                Contract.Ensures(CurrentState == value);
                <a class="userortestcodecovered">_currentState = value;</a>
            <a class="userortestcodecovered">}</a>
        }

        private int _nextState;

        /// &lt;summary&gt;
        /// Next state.
        /// &lt;/summary&gt;
        public int NextState {
            get <a class="button" href="#ID0EL">prev</a>|<span id="ID0EPE"><a class="button" href="#top">top</a>|<a class="button" href="#ID0EPG">next</a></span><a class="userortestcodecovered">{</a> <a class="userortestcodecovered">return _nextState;</a> <a class="userortestcodecovered">}</a>
            protected internal set <a class="button" href="#ID0EL">prev</a>|<span id="ID0EPG"><a class="button" href="#top">top</a>|<a class="button" href="#ID0EUAAC">next</a></span><a class="userortestcodecovered">{</a>
                Contract.Ensures(NextState == value);
                <a class="userortestcodecovered">_nextState = value;</a>
            <a class="userortestcodecovered">}</a>
        }

        /// &lt;summary&gt;
        /// Construct a new State. 
        /// &lt;/summary&gt;
        /// &lt;param name="spaceMin"&gt;&lt;/param&gt;
        /// &lt;param name="spaceMax"&gt;&lt;/param&gt;
        /// &lt;param name="currentState"&gt;&lt;/param&gt;
        <a class="button" href="#ID0EL">prev</a>|<span id="ID0EUAAC"><a class="button" href="#top">top</a></span><a class="userortestcodecovered">public State(int spaceMin = 0, int spaceMax = 1, int currentState = 0)</a> <a class="userortestcodecovered">{</a>
            <a class="userortestcodecovered">SpaceMin = spaceMin;</a>
            <a class="userortestcodecovered">SpaceMax = spaceMax;</a>
            <a class="userortestcodecovered">_currentState = currentState;</a>
        <a class="userortestcodecovered">}</a>

        [ContractInvariantMethod]
        private void ObjInvariant() {
            Contract.Invariant(SpaceMin &lt; SpaceMax);
            Contract.Invariant(SpaceMin &lt;= _currentState &amp;&amp; SpaceMax &gt;= _currentState);
            Contract.Invariant(SpaceMin &lt;= _nextState &amp;&amp; SpaceMax &gt;= _nextState);
        }
    }
}</pre></div></div><hr /><table width="100%"><tr><td valign="top"><span class="copyright">Copyright (c) Microsoft Corporation. All rights reserved.</span><br /><span class="button" onclick="copySourceToClipboard()">Copy full source to clipboard</span></td></tr></table><div id="debugdiv"> </div></body></html>